Add computation rules to suspension and pushout#52
Add computation rules to suspension and pushout#52TimonNajdovski wants to merge 2 commits intomartinescardo:mainfrom
Conversation
I added the missing computation rules to the suspension and pushout types, as suggested in the discord.
Agda/HITs/Lecture4-notes.lagda.md
Outdated
| Push-rec-glue-l : {X : Type} (l : A → X) (r : B → X) (gl : (c : C) → l (f c) ≡ r (g c)) | ||
| → (a : A) → (Push-rec l r gl) (inl a) ≡ l a | ||
| Push-rec-glue-r : {X : Type} (l : A → X) (r : B → X) (gl : (c : C) → l (f c) ≡ r (g c)) | ||
| → (b : B) → (Push-rec l r gl) (inr b) ≡ r b |
There was a problem hiding this comment.
These should be named Push-rec-in{l,r} and there should be a separate rule relating glue and gl.
There was a problem hiding this comment.
You marked this as resolved, did you forget to push the update?
There was a problem hiding this comment.
I marked it as resolved accidentaly, sorry. Thank you for the correction, the update should be pushed now.
| Push-rec-glue : {X : Type} (l : A → X) (r : B → X) (gl : (c : C) → l (f c) ≡ r (g c)) | ||
| → (c : C) → gl c ≡ (l (f c) ≡⟨ ! (Push-rec-inl l r gl (f c)) ⟩ | ||
| Push-rec l r gl (inl (f c)) ≡⟨ ap (Push-rec l r gl) (glue c) ⟩ | ||
| Push-rec l r gl (inr (g c)) ≡⟨ Push-rec-inr l r gl (g c) ⟩ | ||
| r (g c) ∎) |
There was a problem hiding this comment.
An alternative would be to use something like
PathOver (λ A → A) (ap₂ _≡_ (Push-rec-inl l r gl (f c)) (Push-rec-inr l r gl (g c)))
(ap (Push-rec l r gl) (glue c))
(gl c)sadly PathOver is only introduced in the lecture 5 notes.
|
Could someone summarize or point me to the discussion on the discord? |
|
https://discord.com/channels/964553017212956692/970004609458405447/1102358678973198366 Not much discussion, just noticing that some of the computation rules are missing. |
|
I just noticed an issue, there are postulates in the fifth exercise sheet for these same missing computation rules for the suspension and it's creating multiple definitions of the same function. Should we rename the added postulates in the lecture 4 notes or just remove them? |
3 participants
I added the missing computation rules to the suspension and pushout types, as suggested in the discord.